parameterized invariant
Computing Parameterized Invariants of Parameterized Petri Nets
Esparza, Javier, Raskin, Mikhail, Welzel, Christoph
A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are place invariants, P-components, siphons or traps. Recently, Bozga et al. have presented a novel technique for the \emph{parameterized} verification of safety properties of systems with a ring or array architecture. They show that the statement \enquote{for every instance of the parameterized Petri net, all markings satisfying the linear invariants associated to all the P-components, siphons and traps of the instance are safe} can be encoded in \acs{WS1S} and checked using tools like MONA. However, while the technique certifies that this infinite set of linear invariants extracted from P-components, siphons or traps are strong enough to prove safety, it does not return an explanation of this fact understandable by humans. We present a CEGAR loop that constructs a \emph{finite} set of \emph{parameterized} P-components, siphons or traps, whose infinitely many instances are strong enough to prove safety. For this we design parameterization procedures for different architectures.
- North America > United States > New York > New York County > New York City (0.14)
- Europe > Germany > Bavaria > Upper Bavaria > Munich (0.04)
- Asia > Middle East > Israel > Jerusalem District > Jerusalem (0.04)
- (5 more...)